'Weak Dependency Graph [60.0]'
------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(c()) -> mark(f(g(c())))
, active(f(g(X))) -> mark(g(X))
, proper(c()) -> ok(c())
, proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, top(mark(X)) -> top(proper(X))
, top(ok(X)) -> top(active(X))}
Details:
We have computed the following set of weak (innermost) dependency pairs:
{ active^#(c()) -> c_0(f^#(g(c())))
, active^#(f(g(X))) -> c_1(g^#(X))
, proper^#(c()) -> c_2()
, proper^#(f(X)) -> c_3(f^#(proper(X)))
, proper^#(g(X)) -> c_4(g^#(proper(X)))
, f^#(ok(X)) -> c_5(f^#(X))
, g^#(ok(X)) -> c_6(g^#(X))
, top^#(mark(X)) -> c_7(top^#(proper(X)))
, top^#(ok(X)) -> c_8(top^#(active(X)))}
The usable rules are:
{ active(c()) -> mark(f(g(c())))
, active(f(g(X))) -> mark(g(X))
, proper(c()) -> ok(c())
, proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))}
The estimated dependency graph contains the following edges:
{active^#(f(g(X))) -> c_1(g^#(X))}
==> {g^#(ok(X)) -> c_6(g^#(X))}
{proper^#(f(X)) -> c_3(f^#(proper(X)))}
==> {f^#(ok(X)) -> c_5(f^#(X))}
{proper^#(g(X)) -> c_4(g^#(proper(X)))}
==> {g^#(ok(X)) -> c_6(g^#(X))}
{f^#(ok(X)) -> c_5(f^#(X))}
==> {f^#(ok(X)) -> c_5(f^#(X))}
{g^#(ok(X)) -> c_6(g^#(X))}
==> {g^#(ok(X)) -> c_6(g^#(X))}
{top^#(mark(X)) -> c_7(top^#(proper(X)))}
==> {top^#(ok(X)) -> c_8(top^#(active(X)))}
{top^#(mark(X)) -> c_7(top^#(proper(X)))}
==> {top^#(mark(X)) -> c_7(top^#(proper(X)))}
{top^#(ok(X)) -> c_8(top^#(active(X)))}
==> {top^#(ok(X)) -> c_8(top^#(active(X)))}
{top^#(ok(X)) -> c_8(top^#(active(X)))}
==> {top^#(mark(X)) -> c_7(top^#(proper(X)))}
We consider the following path(s):
1) { top^#(mark(X)) -> c_7(top^#(proper(X)))
, top^#(ok(X)) -> c_8(top^#(active(X)))}
The usable rules for this path are the following:
{ active(c()) -> mark(f(g(c())))
, active(f(g(X))) -> mark(g(X))
, proper(c()) -> ok(c())
, proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(c()) -> mark(f(g(c())))
, active(f(g(X))) -> mark(g(X))
, proper(c()) -> ok(c())
, proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))
, top^#(mark(X)) -> c_7(top^#(proper(X)))
, top^#(ok(X)) -> c_8(top^#(active(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{top^#(ok(X)) -> c_8(top^#(active(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{top^#(ok(X)) -> c_8(top^#(active(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
c() = [0]
mark(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [9]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [7]
c_7(x1) = [1] x1 + [3]
c_8(x1) = [1] x1 + [1]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper(c()) -> ok(c())}
and weakly orienting the rules
{top^#(ok(X)) -> c_8(top^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper(c()) -> ok(c())}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
c() = [0]
mark(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [9]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(f(g(X))) -> mark(g(X))}
and weakly orienting the rules
{ proper(c()) -> ok(c())
, top^#(ok(X)) -> c_8(top^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(f(g(X))) -> mark(g(X))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
c() = [0]
mark(x1) = [1] x1 + [4]
f(x1) = [1] x1 + [8]
g(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [4]
ok(x1) = [1] x1 + [4]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [12]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{top^#(mark(X)) -> c_7(top^#(proper(X)))}
and weakly orienting the rules
{ active(f(g(X))) -> mark(g(X))
, proper(c()) -> ok(c())
, top^#(ok(X)) -> c_8(top^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{top^#(mark(X)) -> c_7(top^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
c() = [0]
mark(x1) = [1] x1 + [12]
f(x1) = [1] x1 + [12]
g(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [0]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [1] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(c()) -> mark(f(g(c())))
, proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))}
Weak Rules:
{ top^#(mark(X)) -> c_7(top^#(proper(X)))
, active(f(g(X))) -> mark(g(X))
, proper(c()) -> ok(c())
, top^#(ok(X)) -> c_8(top^#(active(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(c()) -> mark(f(g(c())))
, proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))}
Weak Rules:
{ top^#(mark(X)) -> c_7(top^#(proper(X)))
, active(f(g(X))) -> mark(g(X))
, proper(c()) -> ok(c())
, top^#(ok(X)) -> c_8(top^#(active(X)))}
Details:
The problem is Match-bounded by 5.
The enriched problem is compatible with the following automaton:
{ active_0(2) -> 6
, active_1(2) -> 15
, active_1(9) -> 17
, active_2(9) -> 28
, active_2(32) -> 37
, active_3(32) -> 39
, active_3(41) -> 43
, active_4(40) -> 58
, active_4(41) -> 45
, active_5(40) -> 60
, active_5(61) -> 63
, c_0() -> 2
, c_1() -> 9
, c_2() -> 20
, c_3() -> 35
, c_4() -> 56
, mark_0(2) -> 2
, mark_1(7) -> 6
, mark_1(7) -> 15
, mark_2(18) -> 17
, mark_2(18) -> 28
, mark_3(31) -> 37
, mark_3(31) -> 39
, mark_4(40) -> 43
, mark_4(40) -> 45
, f_1(8) -> 7
, f_2(19) -> 18
, f_2(21) -> 13
, f_2(21) -> 24
, f_3(29) -> 26
, f_3(29) -> 34
, f_3(31) -> 32
, f_4(40) -> 41
, g_1(9) -> 8
, g_2(20) -> 19
, g_2(22) -> 21
, g_3(20) -> 31
, g_3(30) -> 29
, g_4(35) -> 40
, g_4(50) -> 47
, g_4(50) -> 49
, g_5(53) -> 52
, g_5(53) -> 55
, g_5(56) -> 61
, proper_0(2) -> 4
, proper_1(2) -> 11
, proper_1(7) -> 13
, proper_2(7) -> 24
, proper_2(8) -> 21
, proper_2(9) -> 22
, proper_2(18) -> 26
, proper_3(18) -> 34
, proper_3(19) -> 29
, proper_3(20) -> 30
, proper_3(31) -> 47
, proper_4(20) -> 50
, proper_4(31) -> 49
, proper_4(40) -> 52
, proper_5(35) -> 53
, proper_5(40) -> 55
, ok_0(2) -> 2
, ok_0(2) -> 4
, ok_1(9) -> 11
, ok_2(20) -> 22
, ok_3(31) -> 21
, ok_3(32) -> 13
, ok_3(32) -> 24
, ok_3(35) -> 30
, ok_3(35) -> 50
, ok_4(40) -> 29
, ok_4(40) -> 47
, ok_4(40) -> 49
, ok_4(41) -> 26
, ok_4(41) -> 34
, ok_4(56) -> 53
, ok_5(61) -> 52
, ok_5(61) -> 55
, top^#_0(2) -> 1
, top^#_0(4) -> 3
, top^#_0(6) -> 5
, top^#_1(11) -> 10
, top^#_1(13) -> 12
, top^#_1(15) -> 14
, top^#_1(17) -> 16
, top^#_2(24) -> 23
, top^#_2(26) -> 25
, top^#_2(28) -> 27
, top^#_2(37) -> 36
, top^#_3(34) -> 33
, top^#_3(39) -> 38
, top^#_3(43) -> 42
, top^#_3(47) -> 46
, top^#_4(45) -> 44
, top^#_4(49) -> 48
, top^#_4(52) -> 51
, top^#_4(58) -> 57
, top^#_5(55) -> 54
, top^#_5(60) -> 59
, top^#_5(63) -> 62
, c_7_0(3) -> 1
, c_7_1(10) -> 1
, c_7_1(12) -> 5
, c_7_2(23) -> 14
, c_7_2(25) -> 16
, c_7_3(33) -> 27
, c_7_3(46) -> 36
, c_7_4(48) -> 38
, c_7_4(51) -> 42
, c_7_4(51) -> 44
, c_7_5(54) -> 44
, c_8_0(5) -> 1
, c_8_0(5) -> 3
, c_8_1(14) -> 1
, c_8_1(14) -> 3
, c_8_1(16) -> 10
, c_8_2(27) -> 10
, c_8_2(36) -> 12
, c_8_3(38) -> 23
, c_8_3(42) -> 25
, c_8_4(44) -> 33
, c_8_4(57) -> 46
, c_8_5(59) -> 48
, c_8_5(62) -> 51
, c_8_5(62) -> 54}
2) { proper^#(f(X)) -> c_3(f^#(proper(X)))
, f^#(ok(X)) -> c_5(f^#(X))}
The usable rules for this path are the following:
{ proper(c()) -> ok(c())
, proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(c()) -> ok(c())
, proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))
, proper^#(f(X)) -> c_3(f^#(proper(X)))
, f^#(ok(X)) -> c_5(f^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{f^#(ok(X)) -> c_5(f^#(X))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(ok(X)) -> c_5(f^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
c() = [0]
mark(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_2() = [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper^#(f(X)) -> c_3(f^#(proper(X)))}
and weakly orienting the rules
{f^#(ok(X)) -> c_5(f^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(f(X)) -> c_3(f^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
c() = [0]
mark(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_2() = [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper(c()) -> ok(c())}
and weakly orienting the rules
{ proper^#(f(X)) -> c_3(f^#(proper(X)))
, f^#(ok(X)) -> c_5(f^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper(c()) -> ok(c())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
c() = [0]
mark(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [3]
c_1(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_2() = [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))}
Weak Rules:
{ proper(c()) -> ok(c())
, proper^#(f(X)) -> c_3(f^#(proper(X)))
, f^#(ok(X)) -> c_5(f^#(X))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))}
Weak Rules:
{ proper(c()) -> ok(c())
, proper^#(f(X)) -> c_3(f^#(proper(X)))
, f^#(ok(X)) -> c_5(f^#(X))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ c_0() -> 2
, ok_0(2) -> 7
, ok_0(7) -> 7
, f^#_0(2) -> 11
, f^#_0(7) -> 11
, proper^#_0(2) -> 14
, proper^#_0(7) -> 14
, c_5_0(11) -> 11}
3) { proper^#(g(X)) -> c_4(g^#(proper(X)))
, g^#(ok(X)) -> c_6(g^#(X))}
The usable rules for this path are the following:
{ proper(c()) -> ok(c())
, proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(c()) -> ok(c())
, proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))
, proper^#(g(X)) -> c_4(g^#(proper(X)))
, g^#(ok(X)) -> c_6(g^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{g^#(ok(X)) -> c_6(g^#(X))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{g^#(ok(X)) -> c_6(g^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
c() = [0]
mark(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper^#(g(X)) -> c_4(g^#(proper(X)))}
and weakly orienting the rules
{g^#(ok(X)) -> c_6(g^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(g(X)) -> c_4(g^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
c() = [0]
mark(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper(c()) -> ok(c())}
and weakly orienting the rules
{ proper^#(g(X)) -> c_4(g^#(proper(X)))
, g^#(ok(X)) -> c_6(g^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper(c()) -> ok(c())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
c() = [0]
mark(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [2]
proper^#(x1) = [1] x1 + [3]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))}
Weak Rules:
{ proper(c()) -> ok(c())
, proper^#(g(X)) -> c_4(g^#(proper(X)))
, g^#(ok(X)) -> c_6(g^#(X))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))}
Weak Rules:
{ proper(c()) -> ok(c())
, proper^#(g(X)) -> c_4(g^#(proper(X)))
, g^#(ok(X)) -> c_6(g^#(X))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ c_0() -> 2
, ok_0(2) -> 7
, ok_0(7) -> 7
, g^#_0(2) -> 13
, g^#_0(7) -> 13
, proper^#_0(2) -> 14
, proper^#_0(7) -> 14
, c_6_0(13) -> 13}
4) {proper^#(f(X)) -> c_3(f^#(proper(X)))}
The usable rules for this path are the following:
{ proper(c()) -> ok(c())
, proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(c()) -> ok(c())
, proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))
, proper^#(f(X)) -> c_3(f^#(proper(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper^#(f(X)) -> c_3(f^#(proper(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(f(X)) -> c_3(f^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
c() = [0]
mark(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_2() = [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper(c()) -> ok(c())}
and weakly orienting the rules
{proper^#(f(X)) -> c_3(f^#(proper(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper(c()) -> ok(c())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
c() = [0]
mark(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [7]
c_1(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [10]
c_2() = [0]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))}
Weak Rules:
{ proper(c()) -> ok(c())
, proper^#(f(X)) -> c_3(f^#(proper(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))}
Weak Rules:
{ proper(c()) -> ok(c())
, proper^#(f(X)) -> c_3(f^#(proper(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ c_0() -> 2
, ok_0(2) -> 7
, ok_0(7) -> 7
, f^#_0(2) -> 11
, f^#_0(7) -> 11
, proper^#_0(2) -> 14
, proper^#_0(7) -> 14}
5) {proper^#(g(X)) -> c_4(g^#(proper(X)))}
The usable rules for this path are the following:
{ proper(c()) -> ok(c())
, proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(c()) -> ok(c())
, proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))
, proper^#(g(X)) -> c_4(g^#(proper(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper^#(g(X)) -> c_4(g^#(proper(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(g(X)) -> c_4(g^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
c() = [0]
mark(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper(c()) -> ok(c())}
and weakly orienting the rules
{proper^#(g(X)) -> c_4(g^#(proper(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper(c()) -> ok(c())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
c() = [0]
mark(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [4]
proper^#(x1) = [1] x1 + [5]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))}
Weak Rules:
{ proper(c()) -> ok(c())
, proper^#(g(X)) -> c_4(g^#(proper(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, g(ok(X)) -> ok(g(X))
, f(ok(X)) -> ok(f(X))}
Weak Rules:
{ proper(c()) -> ok(c())
, proper^#(g(X)) -> c_4(g^#(proper(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ c_0() -> 2
, ok_0(2) -> 7
, ok_0(7) -> 7
, g^#_0(2) -> 13
, g^#_0(7) -> 13
, proper^#_0(2) -> 14
, proper^#_0(7) -> 14}
6) {active^#(c()) -> c_0(f^#(g(c())))}
The usable rules for this path are the following:
{g(ok(X)) -> ok(g(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ g(ok(X)) -> ok(g(X))
, active^#(c()) -> c_0(f^#(g(c())))}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(c()) -> c_0(f^#(g(c())))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(c()) -> c_0(f^#(g(c())))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
c() = [0]
mark(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
g(x1) = [1] x1 + [1]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {g(ok(X)) -> ok(g(X))}
Weak Rules: {active^#(c()) -> c_0(f^#(g(c())))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {g(ok(X)) -> ok(g(X))}
Weak Rules: {active^#(c()) -> c_0(f^#(g(c())))}
Details:
The problem is Match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ c_0() -> 2
, c_1() -> 8
, g_0(2) -> 4
, g_1(2) -> 5
, g_1(8) -> 7
, ok_0(2) -> 2
, ok_1(5) -> 4
, ok_1(5) -> 5
, active^#_0(2) -> 1
, c_0_0(3) -> 1
, c_0_1(6) -> 1
, f^#_0(2) -> 1
, f^#_0(4) -> 3
, f^#_1(7) -> 6}
7) { active^#(f(g(X))) -> c_1(g^#(X))
, g^#(ok(X)) -> c_6(g^#(X))}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
c() = [0]
mark(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
g(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {g^#(ok(X)) -> c_6(g^#(X))}
Weak Rules: {active^#(f(g(X))) -> c_1(g^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{g^#(ok(X)) -> c_6(g^#(X))}
and weakly orienting the rules
{active^#(f(g(X))) -> c_1(g^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{g^#(ok(X)) -> c_6(g^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
c() = [0]
mark(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [1]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [3]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [3]
g^#(x1) = [1] x1 + [1]
proper^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [3]
top^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ g^#(ok(X)) -> c_6(g^#(X))
, active^#(f(g(X))) -> c_1(g^#(X))}
Details:
The given problem does not contain any strict rules
8) {active^#(f(g(X))) -> c_1(g^#(X))}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
c() = [0]
mark(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
g(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {active^#(f(g(X))) -> c_1(g^#(X))}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(f(g(X))) -> c_1(g^#(X))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(f(g(X))) -> c_1(g^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
c() = [0]
mark(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [0]
g^#(x1) = [1] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {active^#(f(g(X))) -> c_1(g^#(X))}
Details:
The given problem does not contain any strict rules
9) {proper^#(c()) -> c_2()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
c() = [0]
mark(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
g(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {proper^#(c()) -> c_2()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper^#(c()) -> c_2()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(c()) -> c_2()}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
c() = [0]
mark(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
g(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {proper^#(c()) -> c_2()}
Details:
The given problem does not contain any strict rules